Inference at * 2 1 1 1 
Iof proof for Lemma fseg select:

.....assertion..... NILNIL

1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||  ||l2||
5. i:. (i < ||l1||)  (l1[i] = l2[((||l2|| - ||l1||)+i)])
  l1 = nth_tl(||l2|| - ||l1||;l2) 

latex

 by ((BLemma `list_extensionality`) 
CollapseTHEN (Auto)) 

latex

C1: 

C1:   ||l1|| = ||nth_tl(||l2|| - ||l1||;l2)||
C2: 

C2: 6. i : 
C2: 7. i < ||l1||
C2:   l1[i] = nth_tl(||l2|| - ||l1||;l2)[i]
C.

Definitions	nth_tl(n;as), l[i], n+m, n - m, A, False, P  Q, ||as||, , a < b, S  T, |g|, , {x:A| B(x)} , x:A. B(x), x:AB(x), A  B, type List, Type, , t  T, s = t
Lemmas	list extensionality, nth tl wf, nat wf